perm filename WDEL[1,DBL] blob
sn#035520 filedate 1973-07-11 generic text, type T, neo UTF8
(PROGN (LISPXPRIN1 (QUOTE "FILE CREATED ")
T)
(LISPXPRIN1 (QUOTE " 3-APR-73 11:36:28")
T)
(LISPXTERPRI T))
(DEFINEQ
(QA4COUNT
[LAMBDA (X)
(COUNT (T:STRIPALL X])
(ASK
[LAMBDA (X)
[SETQ X (CDR (/MD (NET2LIST X]
(MAPCAR X (FUNCTION PRINT))
(PRIN1 (QUOTE :))
(COND
((NEQ TRACEFILE T)
[MAPCAR X (FUNCTION (LAMBDA (U)
(PRINT U T]
(PRIN1 (QUOTE :)
T)))
(SETQ X (READ))
(COND
((NEQ TRACEFILE T)
(PRINT X)))
(COND
((MEMB (CAR (UNPACK X))
(QUOTE (Y T O)))
(QUOTE TRUE))
((QUOTE FALSE])
(NEWV
[NLAMBDA L
(/SET (QUOTE VERIVARS)
(CONS (CONS (QUOTE VARS)
(UNION L (CDAR VERIVARS)))
(CDR VERIVARS)))
L])
)
(LISPXPRINT (QUOTE VERIFNS)
T)
(RPAQQ VERIFNS (QA4COUNT ASK NEWV))
(LISPXPRINT (QUOTE VERIVARS)
T)
(RPAQQ
VERIVARS
((VARS PROVE PROOFSWITCH EQRULES INEQUALITIES DEDUCE RELCHECK
ANDSPLIT EQSIMP PROOFSIMP PROOFLEIB SIMPONE DONE ASK INSIST
TOPRULES DOWNRULES TRY LEIBF LEIBT LEIBS LEIBB EQTIMESDIVIDE
EQSUBST EQSUBSTRULES SUBSTCAR SUBSTCDR SUBSTCARCDR SUBSTCONS
REMOVE GTQLTQ LTQMANY LTQPLUS FSUBTRACT1 FSUBTRACT2 INEQLEIB
INEQTIMESDIVIDE EQINEQMONOTONE NOTATOM CONSTCAR CONSTCDR
HASSIMP PLUSOP TRYALLFAIL TRYALL PLUSRULES PLUSEMPTY
PLUSSINGLE PLUSZERO PLUSPLUS PLUSMINUS PLUSDIFFERENCE
PLUSCOMBINE PLUSNUMBER TIMESOP TIMESRULES TIMESEMPTY
TIMESSINGLE TIMESZERO TIMESONE TIMESPLUS TIMESTIMES CANCEL
SQRULE TIMESEXP TIMESDIVIDEONE MINUSOP MINUSZERO MINUSMINUS
MINUSPLUS BAGAOP BAGARULES BAGAEMPTY BAGAII BAGAPLUS
BAGAMINUS BACH BAGEX SUBSTOP SUBSTRULES SUBSTEMPTY SUBSTLIST
SUBSTCOMPOSE SUBSTCONST EXPZERO EXPEXP SUBPLUS SUBNUM GCDEQ
ACCH CONSDIFF DIFDIF DIFFRULES DIFFXX DIFFCONS DIFFONE
MAXPLUS MAXONE BAGSTRIP ACCEX EQNUMB SHORTEST SUBSIMP TRYSUB
ARGSIMP TUPSIMP BAGSIMP SETSIMP)
(P (DEFTYPE (QUOTE UNIFY)
(QUOTE TUPLE))
(DEFTYPE (QUOTE REMOVE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE VARSUBST)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MATCH)
(QUOTE TUPLE))
(DEFTYPE (QUOTE COMPOSE)
(QUOTE TUPLE))
[QA4 (QUOTE (WHEN EXP (GTQ ←X ←Y)
INDICATOR MODELVALUE THEN
(ASSERT (LTQ $Y $X)
WRT $VERICON]
[QA4 (QUOTE (WHEN EXP (GT ←X ←Y)
INDICATOR MODELVALUE THEN
(ASSERT (LTQ (PLUS $Y 1)
$X)
WRT $VERICON]
[QA4 (QUOTE (WHEN EXP (LT ←X ←Y)
INDICATOR MODELVALUE THEN
(ASSERT (LTQ (PLUS $X 1)
$Y)
WRT $VERICON]
[QA4 (QUOTE (WHEN EXP (LTQ (PLUS ←X ←Y)
(PLUS ←X ←Z))
INDICATOR MODELVALUE THEN
(ASSERT (LTQ $Y $Z)
WRT $VERICON]
(DEFTYPE (QUOTE GCD)
(QUOTE SET))
(DEFTYPE (QUOTE NEQ)
(QUOTE SET))
(DEFTYPE (QUOTE SUBTRACT)
(QUOTE TUPLE))
(DEFTYPE (QUOTE CONDMAKE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE CONDMAKE1)
(QUOTE TUPLE))
(DEFTYPE (QUOTE EXCHANGE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MAXA)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MAXA)
(QUOTE TUPLE))
(DEFTYPE (QUOTE EXP)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MINUS)
(QUOTE TUPLE))
(DEFTYPE (QUOTE EQ)
(QUOTE SET))
(DEFTYPE (QUOTE ACCESS)
(QUOTE TUPLE))
(DEFTYPE (QUOTE SUBSIMP)
(QUOTE TUPLE))
(DEFTYPE (QUOTE CHANGE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE BAGA)
(QUOTE TUPLE))
(FSETUP VERIVARS))
(PROP HISTORY MATCHASS MATCHGOAL UNIFYASS UNIFYGOAL)))
(RPAQQ PROVE (TUPLE PROOFSWITCH))
[RPAQQ PROOFSWITCH (LAMBDA (←F ←X)
(PROG (DECLARE)
(IF (EQUAL $F (QUOTE EQ))
THEN
(GOAL $EQRULES ($F $X))
ELSE
(GOAL $INEQUALITIES
($F $X)))
(ASSERT ($F $X))
(RETURN ($F $X]
(RPAQQ EQRULES
(TUPLE ANDSPLIT RELCHECK EQTIMESDIVIDE EQSUBST LEIBT LEIBF
LEIBB LEIBS EQSIMP PROOFLEIB))
(RPAQQ INEQUALITIES
(TUPLE ANDSPLIT RELCHECK GTQLTQ LTQMANY FSUBTRACT1 FSUBTRACT2
INEQTIMESDIVIDE EQINEQMONOTONE LTQPLUS PROOFSIMP
PROOFLEIB INEQLEIB))
(RPAQQ DEDUCE (TUPLE RELCHECK ANDSPLIT LTQPLUS NOTATOM CONSTCAR
CONSTCDR))
(RPAQQ RELCHECK [LAMBDA ←X (ISREL? $X])
[RPAQQ ANDSPLIT (LAMBDA (AND ←X ←←Y)
(ATTEMPT (GOAL $GOALCLASS $X)
THEN
(ATTEMPT (GOAL $GOALCLASS
(AND $$Y))
ELSE
(FAIL))
ELSE
(FAIL]
(RPAQQ EQSIMP [LAMBDA (EQ ←X ←Y)
(PROG (DECLARE)
(SETQ ←X ($SIMPONE $X))
(GOAL $EQRULES (EQ $X $Y)))
BACKTRACK])
[RPAQQ PROOFSIMP (LAMBDA (PAND ←X (←F ←Y))
(PROG (DECLARE GOALCLASS1)
(SETQ ←GOALCLASS1 $GOALCLASS)
(ATTEMPT (SETQ ←X ($ARGSIMP $X))
ELSE
(FAIL))
(GOAL $GOALCLASS1 $X]
[RPAQQ PROOFLEIB (LAMBDA (←F ←X)
(PROG (DECLARE)
(EXISTS ($F ←Y))
($ASK (' (EQ $X $Y))
PROVE?)
(GOAL $EQRULES (EQ $X $Y]
[RPAQQ SIMPONE (LAMBDA ←GOAL1
(PROG (DECLARE SIMPGOAL)
(IF (EQUAL (STYPE $GOAL1)
NUMBER)
THEN
(FAIL))
($ASK $GOAL1 SIMPLIFY?)
[SETQ ←SIMPGOAL
(ATTEMPT (GOAL $TOPRULES $GOAL1)
ELSE
($TRY $TOPRULES
(GOAL $DOWNRULES
$GOAL1]
(PUT $GOAL1 SIMPLIFIED $SIMPGOAL WRT
ETERNAL)
(RETURN $SIMPGOAL]
(RPAQQ DONE [LAMBDA ←X (EQUAL (GET $X SIMPLIFIED)
DONE])
[RPAQQ ASK (LAMBDA ←X (IF (LISP ASK $X)
ELSE
(FAIL]
[RPAQQ INSIST (LAMBDA ←X (IF $X ELSE (FAIL]
(RPAQQ TOPRULES
(TUPLE HASSIMP PLUSOP TIMESOP MINUSOP BAGAOP SUBSTOP EXPZERO
EXPEXP SUBPLUS SUBNUM GCDEQ ACCH CONSDIFF DIFDIF
DIFFCONS DIFFONE MAXPLUS MAXONE BAGSTRIP ACCEX EQNUMB))
(RPAQQ DOWNRULES (TUPLE ARGSIMP TUPSIMP BAGSIMP SETSIMP))
(RPAQQ TRY [LAMBDA (TUPLE ←GOALCLASS ←GOAL1)
(ATTEMPT (GOAL $GOALCLASS $GOAL1)
ELSE $GOAL1])
[RPAQQ LEIBF (LAMBDA (EQ (←F ←X)
(←F ←Y))
(PROG (DECLARE)
($ASK (' (EQ $X $Y))
PROVE?)
(GOAL $EQRULES (EQ $X $Y]
[RPAQQ LEIBT (LAMBDA (EQ (TUPLE ←X ←←Z)
(TUPLE ←Y ←←W))
(PROG (DECLARE)
(GOAL $EQRULES (EQ $X $Y))
(GOAL $EQRULES (EQ $Z $W]
[RPAQQ LEIBS (LAMBDA (EQ (SET ←X ←←Z)
(SET ←Y ←←Z))
(GOAL $EQRULES (EQ $X $Y]
[RPAQQ LEIBB (LAMBDA (EQ (BAG ←X ←←Z)
(BAG ←Y ←←Z))
(GOAL $EQRULES (EQ $X $Y]
(RPAQQ EQTIMESDIVIDE [LAMBDA (EQ ←W (TIMES (DIVIDES ←X ←Y)
←←Z))
(GOAL $EQRULES (EQ (TIMES $Y $W)
(TIMES $X $$Z)))
BACKTRACK])
(RPAQQ EQSUBST [LAMBDA (PAND ←Y (EQ (VARSUBST ←S ←X)
←Z))
(GOAL $EQSUBSTRULES $Y])
(RPAQQ EQSUBSTRULES (TUPLE SUBSTCAR SUBSTCDR SUBSTCARCDR SUBSTCONS))
[RPAQQ SUBSTCAR (LAMBDA (EQ (VARSUBST ←S1 (CAR ←X))
(CAR ←Y))
(GOAL $EQRULES (EQ (VARSUBST $S1 $X)
$Y]
[RPAQQ SUBSTCDR (LAMBDA (EQ (VARSUBST ←S1 (CDR ←X))
(CDR ←Y))
(GOAL $EQRULES (EQ (VARSUBST $S1 $X)
$Y]
[RPAQQ SUBSTCARCDR (LAMBDA (EQ (VARSUBST ←S ←U)
(VARSUBST ←S ←V))
(PROG (DECLARE)
(GOAL $DEDUCE (NOT (ATOM $U)))
(GOAL $DEDUCE (NOT (ATOM $V)))
[GOAL $EQRULES
(EQ (VARSUBST $S (CAR $U))
(VARSUBST $S (CAR $V]
(GOAL $EQRULES
(EQ (VARSUBST $S (CDR $U))
(VARSUBST $S (CDR $V]
[RPAQQ SUBSTCONS (LAMBDA (EQ (VARSUBST ←S1 ←X)
←Y)
(PROG (DECLARE)
(GOAL $DEDUCE (NOT (ATOM $X)))
(GOAL $DEDUCE (NOT (ATOM $Y)))
(GOAL (= ($REMOVE EQSUBST FROM
$EQRULES))
(EQ (VARSUBST $S1 (CAR $X))
(CAR $Y)))
(GOAL (= ($REMOVE EQSUBST FROM
$EQRULES))
(EQ (VARSUBST $S1 (CDR $X))
(CDR $Y]
(RPAQQ REMOVE [LAMBDA (TUPLE ←X FROM ←Y)
((QUOTE [LAMBDA (TUPLE ←←U $X ←←V)
(TUPLE $$U $$V])
$Y])
[RPAQQ GTQLTQ (LAMBDA (GTQ ←Y ←X)
(GOAL $INEQUALITIES (LTQ $X $Y]
[RPAQQ LTQMANY (LAMBDA (LTQ ←X ←Y ←Z ←←W)
(PROG (DECLARE)
(GOAL $INEQUALITIES (LTQ $X $Y))
(GOAL $INEQUALITIES
(LTQ $Y $Z $$W]
(RPAQQ LTQPLUS [LAMBDA (LTQ ←I (PLUS ←J ←K))
(GOAL $DEDUCE (AND (LTQ $I $J)
(LTQ 0 $K)))
BACKTRACK])
[RPAQQ FSUBTRACT1 (LAMBDA (←F (SUBTRACT ←X ←Y)
←Z)
(GOAL $GOALCLASS ($F $X (PLUS $Y $Z]
[RPAQQ FSUBTRACT2 (LAMBDA (←F ←X (SUBTRACT ←Y ←Z))
(GOAL $GOALCLASS ($F (PLUS $X $Z)
$Y]
[RPAQQ INEQLEIB (LAMBDA (←L ←X ←Y)
(PROG (DECLARE LOWER UPPER)
(EXISTS ($L ←LOWER ←UPPER))
($ASK PROVE (' (LTQ $X $LOWER))
AND
(' (LTQ $UPPER $Y))
?)
(GOAL $INEQUALITIES
(AND (LTQ $X $LOWER)
(LTQ $UPPER $Y]
(RPAQQ INEQTIMESDIVIDE [LAMBDA (←F ←W (TIMES (DIVIDES ←X ←Y)
←←Z))
[PROG (DECLARE)
(GOAL $DEDUCE (LT 0 $Y))
(GOAL $INEQUALITIES
($F (TIMES $Y $W)
(TIMES $X $$Z]
BACKTRACK])
(RPAQQ EQINEQMONOTONE [LAMBDA
(←L (←F (BAG ←W ←X))
(←F (BAG ←Y ←Z)))
[PROG (DECLARE)
($INSIST (IN $F (TUPLE PLUS TIMES)))
($ASK PROVE (' ($L $W $Y))
AND
(' ($L $X $Z))
?)
(GOAL $GOALCLASS (AND ($L $W $Y)
($L $X $Z]
BACKTRACK])
[RPAQQ NOTATOM (LAMBDA (NOT (ATOM ←X))
(PROG (DECLARE)
(EXISTS (NOT (VAR $X)))
(EXISTS (NOT (CONST $X]
[RPAQQ CONSTCAR (LAMBDA (CONSTEXP (CAR ←X))
(EXISTS (CONSTEXP $X]
[RPAQQ CONSTCDR (LAMBDA (CONSTEXP (CDR ←X))
(EXISTS (CONSTEXP $X]
[RPAQQ HASSIMP (LAMBDA
←X
(IF (NOT (IN (SETQ ←X (GET $X SIMPLIFIED))
(TUPLE DONE NOSUCHPROPERTY)))
THEN $X ELSE (FAIL]
(RPAQQ PLUSOP [LAMBDA (PAND ←Y (PLUS ←←X))
($TRYALLFAIL $PLUSRULES $Y])
[RPAQQ TRYALLFAIL (LAMBDA (TUPLE ←GOALCLASS1 ←GOAL1)
($TRYALL $GOALCLASS1 (GOAL $GOALCLASS1
$GOAL1]
[RPAQQ TRYALL (LAMBDA (TUPLE ←GOALCLASS1 ←GOAL1)
(PROG (DECLARE)
TOP
(ATTEMPT (SETQ ←GOAL1 (GOAL $GOALCLASS1
$GOAL1))
THEN
(GO TOP))
(RETURN $GOAL1]
(RPAQQ PLUSRULES (TUPLE PLUSEMPTY PLUSSINGLE PLUSZERO PLUSPLUS
PLUSMINUS PLUSDIFFERENCE PLUSCOMBINE
PLUSNUMBER))
(RPAQQ PLUSEMPTY [LAMBDA (PLUS)
0])
(RPAQQ PLUSSINGLE [LAMBDA (PLUS ←X)
$X])
[RPAQQ PLUSZERO (LAMBDA (PLUS ←←X 0)
(' (PLUS $$X]
[RPAQQ PLUSPLUS (LAMBDA (PLUS (PLUS ←←X)
←←Y)
(' (PLUS $$X $$Y]
[RPAQQ PLUSMINUS (LAMBDA (PLUS ←X (MINUS ←X)
←←Y)
(' (PLUS $$Y]
[RPAQQ PLUSDIFFERENCE (LAMBDA (PLUS ←X (SUBTRACT ←Y ←Z)
←←W)
($TRY (TUPLE PLUSMINUS)
(' (PLUS $Y $X $$W (MINUS $Z]
[RPAQQ PLUSCOMBINE (LAMBDA (PLUS ←X ←X ←←Y)
($TRYSUB $TIMESRULES ON
(' (TIMES 2 $X))
IN
(' (PLUS (TIMES 2 $X)
$$Y]
(RPAQQ PLUSNUMBER [LAMBDA (PLUS ←X ←Y ←←Z)
(PROG (DECLARE SUM)
($INSIST (EQUAL (STYPE $X)
NUMBER))
($INSIST (EQUAL (STYPE $Y)
NUMBER))
(SETQ ←SUM (PLUS $X $Y))
(RETURN (PLUS $SUM $$Z)))
BACKTRACK])
(RPAQQ TIMESOP [LAMBDA (PAND ←Y (TIMES ←←X))
($TRYALLFAIL $TIMESRULES $Y])
(RPAQQ TIMESRULES
(TUPLE TIMESEMPTY TIMESSINGLE TIMESZERO TIMESONE TIMESPLUS
TIMESTIMES CANCEL SQRULE TIMESEXP TIMESDIVIDEONE))
(RPAQQ TIMESEMPTY [LAMBDA (TIMES)
1])
(RPAQQ TIMESSINGLE [LAMBDA (TIMES ←X)
$X])
(RPAQQ TIMESZERO [LAMBDA (TIMES 0 ←←Y)
0])
[RPAQQ TIMESONE (LAMBDA (TIMES 1 ←←X)
(' (TIMES $$X]
[RPAQQ TIMESPLUS (LAMBDA
(TIMES (PLUS ←X ←←Y)
←←Z)
($TRY $PLUSRULES ($TRYSUB $PLUSRULES ON (' (PLUS $$Y))
IN
(' (PLUS (TIMES $X $$Z)
(TIMES (PLUS $$Y)
$$Z]
[RPAQQ TIMESTIMES (LAMBDA (TIMES (TIMES ←←X)
←←Y)
(' (TIMES $$X $$Y]
[RPAQQ CANCEL (LAMBDA (TIMES ←X (DIVIDES ←Y ←X)
←←Z)
(' (TIMES $Y $$Z]
[RPAQQ SQRULE (LAMBDA (TIMES ←X ←X ←←Y)
($TRY (TUPLE TIMESSINGLE)
(' (TIMES (EXP $X 2)
$$Y]
[RPAQQ TIMESEXP (LAMBDA (TIMES ←X (EXP ←X ←N)
←←Y)
($TRYSUB $PLUSRULES ON (' (PLUS $N 1))
IN
(' (TIMES (EXP $X (PLUS $N 1))
$$Y]
[RPAQQ TIMESDIVIDEONE (LAMBDA (TIMES ←X (DIVIDES 1 ←Y)
←←Z)
(' (TIMES (DIVIDES $X $Y)
$$Z]
[RPAQQ MINUSOP (LAMBDA (MINUS ←X)
(GOAL (TUPLE MINUSZERO MINUSMINUS MINUSPLUS)
(MINUS $X]
(RPAQQ MINUSZERO [LAMBDA (MINUS 0)
0])
(RPAQQ MINUSMINUS [LAMBDA (MINUS (MINUS ←X))
$X])
[RPAQQ MINUSPLUS (LAMBDA (MINUS (PLUS ←X ←←Y))
($TRY $PLUSRULES (PLUS (MINUS $X)
(MINUS (PLUS $$Y]
(RPAQQ BAGAOP [LAMBDA (PAND ←Y (BAGA ←←X))
($TRYALLFAIL $BAGARULES $Y])
(RPAQQ BAGARULES (TUPLE BAGAPLUS BACH BAGEX BAGAEMPTY BAGAII
BAGAMINUS))
[RPAQQ BAGAEMPTY (LAMBDA (BAGA ←A ←J ←I)
(PROG (DECLARE)
(GOAL $DEDUCE (LT $I $J))
(RETURN (BAG]
[RPAQQ BAGAII (LAMBDA (BAGA ←A ←I ←J)
(PROG (DECLARE)
(GOAL $DEDUCE (EQ $I $J))
(RETURN (BAG (ACCESS $A $I]
[RPAQQ BAGAPLUS (LAMBDA (BAGA ←A ←I (PLUS 1 ←J))
(PROG (DECLARE)
(GOAL $DEDUCE (LTQ $I (PLUS 1 $J)))
(RETURN (BAG (ACCESS $A (PLUS $J 1))
(STRIP (BAGA $A $I $J]
[RPAQQ BAGAMINUS (LAMBDA
(BAGA ←A ←I ←J)
(PROG (DECLARE)
(IF (EQUAL (STYPE $J)
IDENT)
ELSE
(FAIL))
(RETURN (BAG (ACCESS $A $J)
(STRIP (BAGA $A $I (SUBTRACT $J 1]
[RPAQQ
BACH
(LAMBDA
(BAGA (CHANGE ←A ←J ←T)
←I ←K)
(PROG
(DECLARE)
[ATTEMPT
(GOAL $DEDUCE (LTQ $I $J $K))
THEN
(RETURN
(=
($TRY
$DIFFRULES
($TRYSUB
(TUPLE ACCH ACCEX)
ON
(' (ACCESS $A $J))
IN
($TRYSUB $BAGARULES ON (' (BAGA $A $I $K))
IN
(' (DIFFERENCE (BAG $T
(STRIP (BAGA $A $I $K)))
(BAG (ACCESS $A $J]
(GOAL $DEDUCE (OR (LT $J $I)
(LT $K $J)))
(RETURN (BAGA $A $I $K]
[RPAQQ BAGEX (LAMBDA (BAGA (EXCHANGE ←A ←I ←J)
←L ←M)
(PROG (DECLARE)
(GOAL $DEDUCE (LTQ $L $I))
(GOAL $DEDUCE (LTQ $J $M))
(RETURN (BAGA $A $L $M]
(RPAQQ SUBSTOP [LAMBDA (PAND (VARSUBST ←←X)
←Y)
(GOAL $SUBSTRULES $Y])
(RPAQQ SUBSTRULES (TUPLE SUBSTEMPTY SUBSTLIST SUBSTCOMPOSE SUBSTCONST)
)
(RPAQQ SUBSTEMPTY [LAMBDA (VARSUBST EMPTY ←X)
$X])
(RPAQQ SUBSTLIST [LAMBDA (VARSUBST (LIST (CONS ←V ←Y))
←V)
(PROG (DECLARE)
(EXISTS (VAR $V))
$Y])
[RPAQQ SUBSTCOMPOSE (LAMBDA (VARSUBST (COMPOSE ←S1 ←S2)
←X)
($TRY $SUBSTRULES
(' (VARSUBST $S1 (VARSUBST $S2 $X]
(RPAQQ SUBSTCONST [LAMBDA (VARSUBST ←S ←Y)
(PROG (DECLARE)
(GOAL $DEDUCE (CONSTEXP $Y))
$Y])
(RPAQQ EXPZERO [LAMBDA (EXP ←X 0)
1])
[RPAQQ EXPEXP (LAMBDA (EXP (EXP ←X ←Y)
←Z)
($TRYSUB $TIMESRULES ON (' (TIMES $Y $Z))
IN
(' (EXP $X (TIMES $Y $Z]
[RPAQQ SUBPLUS (LAMBDA (SUBTRACT ←X ←Y)
($TRY $PLUSRULES (' (PLUS $X (MINUS $Y]
[RPAQQ SUBNUM (LAMBDA (SUBTRACT ←X ←Y)
(PROG (DECLARE)
($INSIST (AND (EQUAL (STYPE $X NUMBER))
(EQUAL (STYPE $Y)
NUMBER)))
(RETURN (= (SUBTRACT $X $Y]
[RPAQQ GCDEQ (LAMBDA (GCD ←X ←Y)
(PROG (DECLARE)
(GOAL $DEDUCE (EQ ←X ←Y))
(RETURN $X]
[RPAQQ ACCH (LAMBDA (ACCESS (CHANGE ←A ←I ←T)
←J)
(PROG (DECLARE)
(ATTEMPT (GOAL $DEDUCE (EQ $I $J))
THEN
(RETURN $T))
(GOAL $DEDUCE (NEQ $I $J))
(RETURN (ACCESS $A $J]
[RPAQQ CONSDIFF (LAMBDA (CONS ←X (DIFFERENCE ←Y ←←Z))
(' (DIFFERENCE (CONS $X $Y)
$$Z]
[RPAQQ DIFDIF (LAMBDA (DIFFERENCE (DIFFERENCE ←X ←←Y)
←←Z)
(' (DIFFERENCE $X $$Y $$Z]
(RPAQQ DIFFRULES (TUPLE DIFFONE DIFFXX DIFFCONS))
(RPAQQ DIFFXX [LAMBDA (DIFFERENCE (BAG ←X ←←Y)
(BAG ←X))
(BAG $$Y])
[RPAQQ DIFFCONS (LAMBDA (DIFFERENCE (CONS ←X ←Y)
(BAG ←X)
←←U)
($TRY (TUPLE DIFFONE)
(' (DIFFERENCE $Y $$U]
(RPAQQ DIFFONE [LAMBDA (DIFFERENCE ←X)
$X])
[RPAQQ MAXPLUS (LAMBDA
(MAXA ←A ←I (PLUS ←J 1))
(PROG (DECLARE)
[ATTEMPT [GOAL $DEDUCE (LTQ (MAXA $A $I $J)
(ACCESS $A (PLUS $J 1]
THEN
(RETURN (ACCESS $A (PLUS $J 1]
(GOAL $DEDUCE (LT (ACCESS $A (PLUS $J 1))
(MAXA $A $I $J)))
(RETURN (MAXA $A $I $J]
[RPAQQ MAXONE (LAMBDA (MAXA ←A ←I ←J)
(PROG (DECLARE)
(GOAL $DEDUCE (EQ $I $J))
(RETURN (ACCESS $I]
(RPAQQ BAGSTRIP [LAMBDA (BAG (STRIP ←X))
$X])
[RPAQQ ACCEX (LAMBDA (ACCESS (EXCHANGE ←A ←I ←J)
←K)
(PROG (DECLARE)
(ATTEMPT (GOAL $DEDUCE (EQ $K $I))
THEN
(RETURN (ACCESS $A $J)))
(ATTEMPT (GOAL $DEDUCE (EQ $K $J))
THEN
(RETURN (ACCESS $A $I)))
(GOAL $DEDUCE (AND (NEQ $K $I)
(NEQ $K $J)))
(RETURN (ACCESS $A $K]
[RPAQQ EQNUMB (LAMBDA ←X (PROG (DECLARE BEST EQSET)
(IF (EQUAL (SETQ ←EQSET (GET $X EQ))
NOSUCHPROPERTY)
THEN
(FAIL))
(SETQ ←BEST ($SHORTEST $EQSET))
(IF (EQUAL $BEST $X)
THEN
(FAIL)
ELSE
(RETURN $BEST]
(RPAQQ
SHORTEST
[LAMBDA
←X
(PROG (DECLARE BEST BESTCOUNT TEMPCOUNT)
(SETQ ←BESTCOUNT 2000)
[MAPC $X
(QUOTE (LAMBDA
←Y
(IF (OR (LT (SETQ ←TEMPCOUNT (LISP QA4COUNT
$Y))
$BESTCOUNT)
(EQUAL (STYPE $Y)
NUMBER))
THEN
(SETQ ←BEST $Y)
(SETQ ←BESTCOUNT $TEMPCOUNT]
$BEST])
[RPAQQ SUBSIMP (LAMBDA (TUPLE ←SUB IN ←EXP)
(SUBST $EXP (TUPLE $SUB ($SIMPONE $SUB]
[RPAQQ TRYSUB (LAMBDA (TUPLE ←GOALCLASS ON ←SUB IN ←EXP)
(SUBST $EXP (TUPLE $SUB ($TRYALL $GOALCLASS
$SUB]
[RPAQQ ARGSIMP (LAMBDA (←F ←X)
(SUBST (' ($F $X))
(TUPLE $X ($SIMPONE $X]
(RPAQQ TUPSIMP [LAMBDA (TUPLE ←←X ←Y ←←Z)
(TUPLE $$X ($SIMPONE $Y)
$$Z)
BACKTRACK])
(RPAQQ BAGSIMP [LAMBDA (BAG ←X ←←Y)
(BAG ($SIMPONE $X)
$$Y)
BACKTRACK])
(RPAQQ SETSIMP [LAMBDA (SET ←X ←←Y)
(SET ($SIMPONE $X)
$$Y)
BACKTRACK])
(DEFTYPE (QUOTE UNIFY)
(QUOTE TUPLE))
(DEFTYPE (QUOTE REMOVE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE VARSUBST)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MATCH)
(QUOTE TUPLE))
(DEFTYPE (QUOTE COMPOSE)
(QUOTE TUPLE))
[QA4 (QUOTE (WHEN EXP (GTQ ←X ←Y)
INDICATOR MODELVALUE THEN (ASSERT (LTQ $Y $X)
WRT $VERICON]
[QA4 (QUOTE (WHEN EXP (GT ←X ←Y)
INDICATOR MODELVALUE THEN
(ASSERT (LTQ (PLUS $Y 1)
$X)
WRT $VERICON]
[QA4 (QUOTE (WHEN EXP (LT ←X ←Y)
INDICATOR MODELVALUE THEN
(ASSERT (LTQ (PLUS $X 1)
$Y)
WRT $VERICON]
[QA4 (QUOTE (WHEN EXP (LTQ (PLUS ←X ←Y)
(PLUS ←X ←Z))
INDICATOR MODELVALUE THEN (ASSERT (LTQ $Y $Z)
WRT $VERICON]
(DEFTYPE (QUOTE GCD)
(QUOTE SET))
(DEFTYPE (QUOTE NEQ)
(QUOTE SET))
(DEFTYPE (QUOTE SUBTRACT)
(QUOTE TUPLE))
(DEFTYPE (QUOTE CONDMAKE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE CONDMAKE1)
(QUOTE TUPLE))
(DEFTYPE (QUOTE EXCHANGE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MAXA)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MAXA)
(QUOTE TUPLE))
(DEFTYPE (QUOTE EXP)
(QUOTE TUPLE))
(DEFTYPE (QUOTE MINUS)
(QUOTE TUPLE))
(DEFTYPE (QUOTE EQ)
(QUOTE SET))
(DEFTYPE (QUOTE ACCESS)
(QUOTE TUPLE))
(DEFTYPE (QUOTE SUBSIMP)
(QUOTE TUPLE))
(DEFTYPE (QUOTE CHANGE)
(QUOTE TUPLE))
(DEFTYPE (QUOTE BAGA)
(QUOTE TUPLE))
(FSETUP VERIVARS)
(DEFLIST(QUOTE(
(MATCHASS
(([! (ASSERT (EQ (VARSUBST (MATCH (CAR PAT)
(CAR ARG))
(CAR PAT))
(CAR ARG]
← TRUE)
([! (ASSERT (EQ (VARSUBST (MATCH (VARSUBST (MATCH (CAR PAT)
(CAR ARG))
(CDR PAT))
(CDR ARG))
(VARSUBST (MATCH (CAR PAT)
(CAR ARG))
(CDR PAT)))
(CDR ARG]
← TRUE)
((! (ASSERT (CONSTEXP ARG)))
← TRUE)
([! (ASSERT (NOT (CONST PAT]
← TRUE)
([! (ASSERT (NOT (ATOM ARG]
← TRUE)
([! (ASSERT (NOT (VAR PAT]
← TRUE)))
(MATCHGOAL
(((! (GOAL $PROVE
(EQ (VARSUBST (COMPOSE
(MATCH (VARSUBST (MATCH (CAR PAT)
(CAR ARG))
(CDR PAT))
(CDR ARG))
(MATCH (CAR PAT)
(CAR ARG)))
PAT)
ARG)))
← π)))
(UNIFYASS (((! (ASSERT (NEQ X Y)))
← TRUE)
([! (ASSERT (NOT (VAR X]
← TRUE)
([! (ASSERT (NOT (VAR Y]
← TRUE)
([! (ASSERT (NOT (ATOM X]
← TRUE)
([! (ASSERT (NOT (ATOM Y]
← TRUE)
[[! (SETQQ ←M1 (UNIFY (CAR X)
(CAR Y]
←
(UNIFY (TUPLE (CAR X)
(CAR Y]
([! (ASSERT (EQ (VARSUBST $M1 (CAR X))
(VARSUBST $M1 (CAR Y]
← TRUE)
[[! (SETQ ←M2 (' (UNIFY (VARSUBST $M1 (CDR X))
(VARSUBST $M1 (CDR Y]
←
(UNIFY (TUPLE (VARSUBST $M1 (CDR X))
(VARSUBST $M1 (CDR Y]
([! (ASSERT (EQ (VARSUBST $M2 (VARSUBST $M1 (CDR X)))
(VARSUBST $M2 (VARSUBST $M1 (CDR Y]
← TRUE)))
(UNIFYGOAL (([! (GOAL $EQRULES (EQ (VARSUBST (COMPOSE $M2 $M1)
X)
(VARSUBST (COMPOSE $M2 $M1)
Y]
← π)))
))(QUOTE HISTORY))
STOP